﻿// This project type requires the F# PowerPack at http://fsharppowerpack.codeplex.com/releases
// Learn more about F# at http://fsharp.net
// Original project template by Jomo Fisher based on work of Brian McNamara, Don Syme and Matt Valerio
// This posting is provided "AS IS" with no warranties, and confers no rights.
module CoqAuWin.Main

open System
open System.IO
open Microsoft.FSharp.Text.Lexing

open Ast
open Lexer
open Parser
open Coq.MonoDevelop.Scope


printfn "Calculator"

let rec GetTokens lexbuff =
    seq { let tok = Lexer.tokenize(lexbuff) 
          match tok with 
          | token.EOF(Some tokinner) -> 
                yield tokinner,lexbuff
                yield token.EOF(None),lexbuff 
          | token.EOF(None) ->
                yield token.EOF(None),lexbuff
          | _ -> 
                yield tok,lexbuff
                yield! GetTokens lexbuff
        }

let GetToknesFromString str = 
    let lexbuff = LexBuffer<char>.FromString(str)
    GetTokens lexbuff 



let Parse str = 
    try
        //printfn "Lexing [%s]" str
        let lexbuff = LexBuffer<char>.FromString(str)
        setInitialPos lexbuff ""
        //for tok,lexbuff in GetToknesFromString(str) do
        //    printfn " %A - %A:%A" tok lexbuff.StartPos.pos_cnum lexbuff.EndPos.pos_cnum 
                
        //printfn "Parsing..."
        let equation = Parser.start Lexer.tokenize lexbuff
        //printfn "Tree: %A" equation
        //printfn "Parsed OK"

        //printfn "Creating scopes..."
        //let scope = CoqASTWalker equation 
        //printfn "%A" scope
        
        Some(equation)
    with ex ->
        //printfn "Unhandled Exception: %s" ex.Message
        None

let ParseDbg str =
    try
        //printfn "Lexing [%s]" str
        let lexbuff = LexBuffer<char>.FromString(str)
        setInitialPos lexbuff ""
        for tok,lexbuff in GetToknesFromString(str) do
            printfn " %A - %A:%A" tok lexbuff.StartPos.pos_cnum lexbuff.EndPos.pos_cnum 
                
        printfn "Parsing..."
        let equation = Parser.start Lexer.tokenize lexbuff
        //printfn "Tree: %A" equation
        printfn "Parsed OK"

        //printfn "Creating scopes..."
        //let scope = CoqASTWalker equation 
        //printfn "%A" scope
        
        Some(equation)
    with ex ->
        //printfn "Unhandled Exception: %s" ex.Message
        None

let ParseCSHARP str = 
    match (Parse str) with
    | Some (v)  -> v
    | None      -> Unchecked.defaultof<_>

let ParseFile fileName =
    let str = File.ReadAllText fileName
    Parse str

let Test2() = 
    let mutable str = "";
    while (true) do
        match Console.ReadLine() with
        | "quit" -> ()
        | ";" ->
            try
                printfn "Lexing [%s]" str
                let lexbuff = LexBuffer<char>.FromString(str)
                for tok,lexbuff in GetToknesFromString(str) do
                    printfn " %A - %A:%A" tok lexbuff.StartPos.pos_cnum lexbuff.EndPos.pos_cnum 
                
                printfn "Parsing..."
                let equation = Parser.start Lexer.tokenize lexbuff

                printfn "Tree: %A" equation
            
            with ex ->
                printfn "Unhandled Exception: %s" ex.Message
            str <- ""
        | expr ->
            str <- str + expr;


let rec Test() =
    let mutable lineinput = Console.ReadLine()
    for tok,lexbuff in GetToknesFromString(lineinput) do
        printfn " %A - %A:%A" tok lexbuff.StartPos.pos_cnum lexbuff.EndPos.pos_cnum 

    printfn "Parsing..."
    
    try
        let lexbuff = LexBuffer<char>.FromString(lineinput)
        let equation = Parser.start Lexer.tokenize lexbuff
        printf "%A" equation
    with ex ->
            printfn "Unhandled Exception: %s" ex.Message
    
    Test()


let rec readAndProcess() =
    printf ":"
    match Console.ReadLine() with
    | "quit" -> ()
    | expr ->
        try
            printfn "Lexing [%s]" expr
            let lexbuff = LexBuffer<char>.FromString(expr)
            
            printfn "Parsing..."
            let equation = Parser.start Lexer.tokenize lexbuff
            
            printfn "Evaluating Equation..."
//            let result = evalEquation equation
            let result = "in construction"
            
            printfn "Result: %s" (result.ToString())
            
        with ex ->
            printfn "Unhandled Exception: %s" ex.Message

        readAndProcess()

//readAndProcess()